(e.P(e) a.f(a) e'.Q(e')) with R
== Bij({e:E| P(e)} ;{e':E| Q(e')} ;a.f(a))
== & (e:{e:E| P(e)} . e c f(e) & R(val(e),val(f(e)))) 

latex

---

clarification:

causal-bijection(es;a.f(a);e.P(e);e'.Q(e');R)
== Bij({e:es-E(es)| P(e)} ;{e':es-E(es)| Q(e')} ;a.f(a))
== & (e:{e:es-E(es)| P(e)} . es-causle(es;e;f(e)) & R(es-val(es; e),es-val(es; f(e)))) 

latex

Definitions	Bij(A;B;f), x.A(x), x:A. B(x), {x:A| B(x)} , E, P & Q, e c e', f(a), val(e)
FDL editor aliases	causal-bijection